Il lambda calcolo (anche scritto λ-calcolo) è un formalismo matematico creato nel 1936 da Alonzo Church come rappresentazione rigorosa della computazione tramite l'applicazione ripetuta di regole su funzioni.
È un sistema formale straordinariamente minimalista, come vedremo.
Si definisce λ-termine qualunque fbf a partire dalla seguente grammatica:
T ::= V | λV.T | (T T)
Dove V denota una variabile appartenente ad un insieme infinito di variabili.
Una definizione più intuitiva di quanto scritto sopra è la seguente:
Un λ-termine può essere un nome di variabile, l'astrazione di un terine rispetto ad una variabile, o l'applicazione di un termine come argomento di un altro
Una variabile è fondamentalmente un identificatore
x
Una funzione è così definita
λx.x
In questo caso la funzione prende una variabile x e restituisce x (funzione identità)
Applichiamo la funzione alla variabile a
(λx.x)a
Il risultato dell'applicazione è chiaramente a.
Ma cerchiamo di analizzare le regole del λ-calcolo
1. α-conversione
Permette di rinominare le variabili
λx.x ≡ λy. y
2. β-riduzione
Implementa il passo di computazione. Se lo applichiamo alla funzione identità, sostituisce (λx.x)a con a.
Vediamo un esempio più interessante.
λn.n+1 è la funzione che restituisce il numero successivo alla variabile n. Applicata a 4
(λn.n+1)4
-> 4+1
-> 5
3. η-conversione
Afferma che una funzione che prende un argomento e poi lo passa subito a un’altra funzione è uguale a quella funzione stessa (se non lo modifica).
Permette di "rimuovere" un involucro che non fa altro che il passacarte tra la funzione chiamante e la chiamata.
E' inoltre importante comprendere le differenze tra variabili legate (bound) e libere (unbound).
Nell'esempio λx.x + y la variabile x è bound dato che appare dopo il λx, e quindi è il parametro della funzione. y è unbound e non definita qui, evidentemente il suo significato viene deciso altrove. Vediamo con un esempio a più livelli.
Consideriamo la funzione λx. (λy. x + y):
Nella funzione esterna λx.(...):
- x è bound
- y è unbound
Nella funzione interna λy. x + y:
- y è bound (legato a λy)
- x è unbound
Nota: Il concetto di bound e unbound è fondamentale perché nelle α-conversioni si possono rinominare le bound senza cambiare significato. Se confondessimo una bound con una unbound, rischieremmo di "catturare" variabili per sbaglio. Questo è un fenomeno che invalida la correttezza dei nostri calcoli.
Abbiamo visto brevemente il concetto del λ-calcolo, che come detto prima, è già Turing-completo. In teoria potremmo scrivere tutti i programmi del mondo in λ-calcolo, ma è scomodo e spesso il risultato è lungo e poco chiaro da comprendere. Questo è un formalismo matematico che è stato creato per descrivere in maniera completa e rigorosa la computazione, non per scrivere programmi. In un altro articolo, vedremo formalismi più potenti e dotati di astrazioni che ci consentiranno di rendere più semanticamente esplicito il significato del nostro codice, rendendolo più espressivo ed implementativamente elegante.